R:Realizer.
(R-size(R)  1)
 (ix:(:Id  Id).
 (ix  dom(R-discrete(R)))
  (ix ~ <R-loc(R), if Reffect?(R) then Reffect-x(R) else Rinit-x(R) fi >)) 

latex

Definitions

ff, tt, if b then t else f fi , A, Top, T, P  Q, P  Q, {T}, SQType(T), True, P & Q, P  Q, x. t(x), , t  T, P  Q, x:A. B(x), Y, reduce(f;k;as), deq-member(eq;x;L), , x  dom(f), t.2, t.1, Unit, , False, Rinit?(x1), Reffect?(x1), b, , x(s),

Lemmas

pi2 wf, pi1 wf, Id sq, Rinit-x wf, Reffect-x wf, Rplus-implies, Rnone? wf, Rnone-implies, R-loc wf, fpf-single-dom, assert of bnot, and functionality wrt iff, assert of band, bnot thru bor, true wf, squash wf, eqff to assert, assert of bor, eqtt to assert, iff transitivity, bool sq, bool cases, not wf, bnot wf, band wf, Rinit? wf, Reffect? wf, bor wf, es realizer wf, nat plus wf, R-size wf, le wf, Id wf, top wf, fpf wf, bool wf, fpf-trivial-subtype-top, R-discrete wf, id-deq wf, product-deq wf, fpf-dom wf, assert wf, R-discrete-base